Problem:
 a__f(a(),X,X) -> a__f(X,a__b(),b())
 a__b() -> a()
 mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
 mark(b()) -> a__b()
 mark(a()) -> a()
 a__f(X1,X2,X3) -> f(X1,X2,X3)
 a__b() -> b()

Proof:
 Complexity Transformation Processor:
  strict:
   a__f(a(),X,X) -> a__f(X,a__b(),b())
   a__b() -> a()
   mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
   mark(b()) -> a__b()
   mark(a()) -> a()
   a__f(X1,X2,X3) -> f(X1,X2,X3)
   a__b() -> b()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [mark](x0) = x0,
     
     [f](x0, x1, x2) = x0 + x1 + x2 + 8,
     
     [b] = 0,
     
     [a__b] = 1,
     
     [a__f](x0, x1, x2) = x0 + x1 + x2 + 14,
     
     [a] = 4
    orientation:
     a__f(a(),X,X) = 2X + 18 >= X + 15 = a__f(X,a__b(),b())
     
     a__b() = 1 >= 4 = a()
     
     mark(f(X1,X2,X3)) = X1 + X2 + X3 + 8 >= X1 + X2 + X3 + 14 = a__f(X1,mark(X2),X3)
     
     mark(b()) = 0 >= 1 = a__b()
     
     mark(a()) = 4 >= 4 = a()
     
     a__f(X1,X2,X3) = X1 + X2 + X3 + 14 >= X1 + X2 + X3 + 8 = f(X1,X2,X3)
     
     a__b() = 1 >= 0 = b()
    problem:
     strict:
      a__b() -> a()
      mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
      mark(b()) -> a__b()
      mark(a()) -> a()
     weak:
      a__f(a(),X,X) -> a__f(X,a__b(),b())
      a__f(X1,X2,X3) -> f(X1,X2,X3)
      a__b() -> b()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [mark](x0) = x0 + 57,
       
       [f](x0, x1, x2) = x0 + x1 + x2 + 16,
       
       [b] = 0,
       
       [a__b] = 0,
       
       [a__f](x0, x1, x2) = x0 + x1 + x2 + 16,
       
       [a] = 0
      orientation:
       a__b() = 0 >= 0 = a()
       
       mark(f(X1,X2,X3)) = X1 + X2 + X3 + 73 >= X1 + X2 + X3 + 73 = a__f(X1,mark(X2),X3)
       
       mark(b()) = 57 >= 0 = a__b()
       
       mark(a()) = 57 >= 0 = a()
       
       a__f(a(),X,X) = 2X + 16 >= X + 16 = a__f(X,a__b(),b())
       
       a__f(X1,X2,X3) = X1 + X2 + X3 + 16 >= X1 + X2 + X3 + 16 = f(X1,X2,X3)
       
       a__b() = 0 >= 0 = b()
      problem:
       strict:
        a__b() -> a()
        mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
       weak:
        mark(b()) -> a__b()
        mark(a()) -> a()
        a__f(a(),X,X) -> a__f(X,a__b(),b())
        a__f(X1,X2,X3) -> f(X1,X2,X3)
        a__b() -> b()
      Splitting Processor:
       strict:
        a__b() -> a()
       weak:
        mark(b()) -> a__b()
        mark(a()) -> a()
        a__f(a(),X,X) -> a__f(X,a__b(),b())
        a__f(X1,X2,X3) -> f(X1,X2,X3)
        a__b() -> b()
        mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
       Matrix Interpretation Processor:
        dimension: 4
        max_matrix:
         [1 1 0 1]
         [0 1 0 0]
         [0 0 0 1]
         [0 0 0 0]
         interpretation:
                       [1 1 0 0]     [0]
                       [0 1 0 0]     [1]
          [mark](x0) = [0 0 0 0]x0 + [0]
                       [0 0 0 0]     [0],
          
                            [1 0 0 0]     [1 0 0 0]     [1 0 0 1]     [0]
                            [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [1]
          [f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2 + [0]
                            [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0],
          
                [0]
                [0]
          [b] = [0]
                [0],
          
                   [0]
                   [0]
          [a__b] = [0]
                   [0],
          
                               [1 0 0 0]     [1 0 0 0]     [1 1 0 1]     [0]
                               [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [1]
          [a__f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 1]x1 + [0 0 0 0]x2 + [0]
                               [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0],
          
                [0]
                [0]
          [a] = [0]
                [0]
         orientation:
                              [1 0 0 0]     [1 1 0 0]     [1 1 0 1]     [1]    [1 0 0 0]     [1 1 0 0]     [1 1 0 1]     [0]                       
                              [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [2]    [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [2]                       
          mark(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = a__f(X1,mark(X2),X3)
                              [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]                       
          
                   [0]    [0]      
                   [0]    [0]      
          a__b() = [0] >= [0] = a()
                   [0]    [0]      
          
                      [0]    [0]         
                      [1]    [0]         
          mark(b()) = [0] >= [0] = a__b()
                      [0]    [0]         
          
                      [0]    [0]      
                      [1]    [0]      
          mark(a()) = [0] >= [0] = a()
                      [0]    [0]      
          
                          [2 1 0 1]    [0]    [1 0 0 0]    [0]                     
                          [0 2 0 0]    [1]    [0 0 0 0]    [1]                     
          a__f(a(),X,X) = [0 0 0 1]X + [0] >= [0 0 0 0]X + [0] = a__f(X,a__b(),b())
                          [0 0 0 0]    [0]    [0 0 0 0]    [0]                     
          
                           [1 0 0 0]     [1 0 0 0]     [1 1 0 1]     [0]    [1 0 0 0]     [1 0 0 0]     [1 0 0 1]     [0]              
                           [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [1]    [0 0 0 0]     [0 1 0 0]     [0 1 0 0]     [1]              
          a__f(X1,X2,X3) = [0 0 0 0]X1 + [0 0 0 1]X2 + [0 0 0 0]X3 + [0] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 + [0] = f(X1,X2,X3)
                           [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]    [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]              
          
                   [0]    [0]      
                   [0]    [0]      
          a__b() = [0] >= [0] = b()
                   [0]    [0]      
         problem:
          strict:
           
          weak:
           mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
           a__b() -> a()
           mark(b()) -> a__b()
           mark(a()) -> a()
           a__f(a(),X,X) -> a__f(X,a__b(),b())
           a__f(X1,X2,X3) -> f(X1,X2,X3)
           a__b() -> b()
         Qed
        
        strict:
         mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
        weak:
         a__b() -> a()
         mark(b()) -> a__b()
         mark(a()) -> a()
         a__f(a(),X,X) -> a__f(X,a__b(),b())
         a__f(X1,X2,X3) -> f(X1,X2,X3)
         a__b() -> b()
        Matrix Interpretation Processor:
         dimension: 3
         max_matrix:
          [1 1 1]
          [0 0 0]
          [0 0 0]
          interpretation:
                        [1 0 0]     [0]
           [mark](x0) = [0 0 0]x0 + [1]
                        [0 0 0]     [1],
           
                             [1 1 1]     [1 0 0]     [1 1 1]  
           [f](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                             [0 0 0]     [0 0 0]     [0 0 0]  ,
           
                 [1]
           [b] = [0]
                 [0],
           
                    [1]
           [a__b] = [1]
                    [1],
           
                                [1 1 1]     [1 0 0]     [1 1 1]  
           [a__f](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
                                [0 0 0]     [0 0 0]     [0 0 0]  ,
           
                 [0]
           [a] = [1]
                 [1]
          orientation:
                    [1]    [0]      
           a__b() = [1] >= [1] = a()
                    [1]    [1]      
           
                       [1]    [1]         
           mark(b()) = [1] >= [1] = a__b()
                       [1]    [1]         
           
                       [0]    [0]      
           mark(a()) = [1] >= [1] = a()
                       [1]    [1]      
           
                           [2 1 1]    [2]    [1 1 1]    [2]                     
           a__f(a(),X,X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__f(X,a__b(),b())
                           [0 0 0]    [0]    [0 0 0]    [0]                     
           
                            [1 1 1]     [1 0 0]     [1 1 1]      [1 1 1]     [1 0 0]     [1 1 1]                
           a__f(X1,X2,X3) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = f(X1,X2,X3)
                            [0 0 0]     [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]     [0 0 0]                
           
                    [1]    [1]      
           a__b() = [1] >= [0] = b()
                    [1]    [0]      
           
                               [1 1 1]     [1 0 0]     [1 1 1]     [0]    [1 1 1]     [1 0 0]     [1 1 1]                         
           mark(f(X1,X2,X3)) = [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 + [1] >= [0 0 0]X1 + [0 0 0]X2 + [0 0 0]X3 = a__f(X1,mark(X2),X3)
                               [0 0 0]     [0 0 0]     [0 0 0]     [1]    [0 0 0]     [0 0 0]     [0 0 0]                         
          problem:
           strict:
            
           weak:
            a__b() -> a()
            mark(b()) -> a__b()
            mark(a()) -> a()
            a__f(a(),X,X) -> a__f(X,a__b(),b())
            a__f(X1,X2,X3) -> f(X1,X2,X3)
            a__b() -> b()
            mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
          Qed